YES 11.118 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((readDec :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\ndn * radix + d

is transformed to
readInt0 radix n d = n * radix + d

The following Lambda expression
\vu77
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt1 radix digToInt vu77 = 
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

The following Lambda expression
\dfromEnum d - fromEnum_0

is transformed to
readDec0 d = fromEnum d - fromEnum_0

The following Lambda expression
\vu68
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull0 vu68 = 
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule Main
  ((readDec :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt10 radix digToInt (ds,r) = (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
readInt10 radix digToInt _ = []

The following Case expression
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull00 (cs@(_ : _),t) = (cs,t: []
nonnull00 _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ BR

mainModule Main
  ((readDec :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
cs@(vy : vz)

is replaced by the following term
vy : vz

The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((readDec :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

span3 p [] = ([],[])
span3 xx xy = span2 xx xy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ LetRed

mainModule Main
  ((readDec :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

are unpacked to the following functions on top level
span2Ys xz yu = span2Ys0 xz yu (span2Vu43 xz yu)

span2Vu43 xz yu = span xz yu

span2Zs xz yu = span2Zs0 xz yu (span2Vu43 xz yu)

span2Span0 xz yu p ww wx True = ([],ww : wx)

span2Span1 xz yu p ww wx True = (ww : span2Ys xz yu,span2Zs xz yu)
span2Span1 xz yu p ww wx False = span2Span0 xz yu p ww wx otherwise

span2Zs0 xz yu (wz,zs) = zs

span2Ys0 xz yu (ys,wy) = ys



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
HASKELL
                      ↳ NumRed

mainModule Main
  ((readDec :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule Main
  (readDec :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs0(Char(Succ(yv7000)), yv71, yv72, yv73) → new_span2Zs00(yv7000, yv71, yv7000, yv72, yv73)
new_span2Zs00(yv92, yv93, Succ(yv940), Zero, yv96) → new_span2Zs01(yv92, yv93, Succ(yv92), Succ(yv96))
new_span2Zs01(yv113, yv114, Zero, Zero) → new_span2Zs03(yv113, yv114)
new_span2Zs(:(yv600, yv601)) → new_span2Zs0(yv600, yv601, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs02(yv92, yv93, yv96) → new_span2Zs01(yv92, yv93, Succ(yv92), Succ(yv96))
new_span2Zs01(yv113, yv114, Succ(yv1150), Succ(yv1160)) → new_span2Zs01(yv113, yv114, yv1150, yv1160)
new_span2Zs00(yv92, yv93, Zero, Zero, yv96) → new_span2Zs02(yv92, yv93, yv96)
new_span2Zs01(yv113, yv114, Zero, Succ(yv1160)) → new_span2Zs(yv114)
new_span2Zs00(yv92, yv93, Succ(yv940), Succ(yv950), yv96) → new_span2Zs00(yv92, yv93, yv940, yv950, yv96)
new_span2Zs03(yv113, yv114) → new_span2Zs(yv114)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yv890), Succ(yv900)) → new_primMinusNat(yv890, yv900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv1980), Succ(yv18200)) → new_primPlusNat(yv1980, yv18200)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv17600), yv175) → new_primMulNat(yv17600, yv175)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldl(yv145, yv146, yv147, yv148, Succ(yv1490), Zero, yv151, ba) → new_foldl0(yv145, yv146, yv147, yv148, Succ(yv147), Succ(yv151), ba)
new_foldl2(yv175, yv176, yv177, yv178, yv181, bb) → new_foldl4(yv175, yv176, new_pt(yv177, bb), yv178, bb)
new_foldl(yv145, yv146, yv147, yv148, Succ(yv1490), Succ(yv1500), yv151, ba) → new_foldl(yv145, yv146, yv147, yv148, yv1490, yv1500, yv151, ba)
new_foldl(yv145, yv146, yv147, yv148, Zero, Zero, yv151, ba) → new_foldl1(yv145, yv146, yv147, yv148, yv151, ba)
new_foldl6(yv132, yv139, Char(Succ(yv13500)), yv136, yv137, yv138, bd) → new_foldl(yv132, yv139, yv13500, yv136, yv13500, yv137, yv138, bd)
new_foldl1(yv145, yv146, yv147, yv148, yv151, ba) → new_foldl0(yv145, yv146, yv147, yv148, Succ(yv147), Succ(yv151), ba)
new_foldl3(yv175, yv176, yv177, yv178, bb) → new_foldl2(yv175, yv176, yv177, yv178, new_span2Zs1(yv178), bb)
new_foldl5(yv191, yv192, yv193, yv194, yv195, yv196, yv197, bc) → new_foldl6(yv191, new_readInt0(yv191, yv192, yv193, bc), yv194, yv195, yv196, yv197, bc)
new_foldl0(yv175, yv176, yv177, yv178, Zero, Succ(yv1800), bb) → new_foldl2(yv175, yv176, yv177, yv178, new_span2Zs1(yv178), bb)
new_foldl0(yv175, yv176, yv177, yv178, Succ(yv1790), Succ(yv1800), bb) → new_foldl0(yv175, yv176, yv177, yv178, yv1790, yv1800, bb)
new_foldl0(yv175, yv176, yv177, yv178, Zero, Zero, bb) → new_foldl3(yv175, yv176, yv177, yv178, bb)
new_foldl4(yv175, yv176, yv182, :(yv1780, yv1781), bb) → new_foldl5(yv175, yv176, yv182, yv1780, yv1781, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))), bb)

The TRS R consists of the following rules:

new_span2Zs05(yv92, yv93, Succ(yv940), Zero, yv96) → new_span2Zs08(yv92, yv93, yv96)
new_readInt0(yv175, Neg(yv1760), Neg(yv1820), ty_Int) → Neg(new_primPlusNat0(new_primMulNat0(yv1760, yv175), yv1820))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_pt(yv61, ty_Int) → new_primMinusInt(yv61, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))
new_primMulNat0(Succ(yv17600), yv175) → new_primPlusNat0(new_primMulNat0(yv17600, yv175), Succ(yv175))
new_primMulNat0(Zero, yv175) → Zero
new_primMinusNat0(Zero, Succ(yv900)) → Neg(Succ(yv900))
new_primPlusNat0(Succ(yv1980), Succ(yv18200)) → Succ(Succ(new_primPlusNat0(yv1980, yv18200)))
new_primMinusInt(yv89, yv90) → new_primMinusNat0(yv89, yv90)
new_span2Zs05(yv92, yv93, Zero, Zero, yv96) → new_span2Zs08(yv92, yv93, yv96)
new_span2Zs05(yv92, yv93, Succ(yv940), Succ(yv950), yv96) → new_span2Zs05(yv92, yv93, yv940, yv950, yv96)
new_span2Zs010(yv113, yv114) → new_span2Zs06(yv113, yv114, new_span2Zs1(yv114))
new_span2Zs04(Char(Zero), yv71, yv72, yv73) → :(Char(Zero), yv71)
new_readInt0(yv175, Pos(yv1760), Neg(yv1820), ty_Int) → new_primMinusNat0(new_primMulNat0(yv1760, yv175), yv1820)
new_readInt0(yv175, Neg(yv1760), Pos(yv1820), ty_Int) → new_primMinusNat0(yv1820, new_primMulNat0(yv1760, yv175))
new_span2Zs09(yv113, yv114, Succ(yv1150), Succ(yv1160)) → new_span2Zs09(yv113, yv114, yv1150, yv1160)
new_span2Zs07(yv92, yv93) → :(Char(Succ(yv92)), yv93)
new_primPlusNat0(Zero, Zero) → Zero
new_span2Zs09(yv113, yv114, Succ(yv1150), Zero) → new_span2Zs07(yv113, yv114)
new_span2Zs08(yv92, yv93, yv96) → new_span2Zs09(yv92, yv93, Succ(yv92), Succ(yv96))
new_span2Zs1([]) → []
new_span2Zs1(:(yv600, yv601)) → new_span2Zs04(yv600, yv601, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs05(yv92, yv93, Zero, Succ(yv950), yv96) → new_span2Zs07(yv92, yv93)
new_span2Zs09(yv113, yv114, Zero, Succ(yv1160)) → new_span2Zs010(yv113, yv114)
new_readInt0(yv175, Pos(yv1760), Pos(yv1820), ty_Int) → Pos(new_primPlusNat0(new_primMulNat0(yv1760, yv175), yv1820))
new_pt(yv61, ty_Integer) → error([])
new_readInt0(yv175, yv176, yv182, ty_Integer) → error([])
new_primMinusNat0(Succ(yv890), Zero) → Pos(Succ(yv890))
new_span2Zs09(yv113, yv114, Zero, Zero) → new_span2Zs010(yv113, yv114)
new_primPlusNat0(Zero, Succ(yv18200)) → Succ(yv18200)
new_primPlusNat0(Succ(yv1980), Zero) → Succ(yv1980)
new_span2Zs04(Char(Succ(yv7000)), yv71, yv72, yv73) → new_span2Zs05(yv7000, yv71, yv7000, yv72, yv73)
new_primMinusNat0(Succ(yv890), Succ(yv900)) → new_primMinusNat0(yv890, yv900)
new_span2Zs06(yv113, yv114, yv118) → yv118

The set Q consists of the following terms:

new_span2Zs08(x0, x1, x2)
new_span2Zs09(x0, x1, Zero, Succ(x2))
new_span2Zs04(Char(Succ(x0)), x1, x2, x3)
new_primMinusInt(x0, x1)
new_readInt0(x0, Neg(x1), Neg(x2), ty_Int)
new_span2Zs05(x0, x1, Succ(x2), Zero, x3)
new_span2Zs05(x0, x1, Zero, Succ(x2), x3)
new_primMinusNat0(Succ(x0), Zero)
new_span2Zs06(x0, x1, x2)
new_span2Zs09(x0, x1, Zero, Zero)
new_span2Zs1(:(x0, x1))
new_span2Zs04(Char(Zero), x0, x1, x2)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_span2Zs010(x0, x1)
new_primMinusNat0(Zero, Zero)
new_readInt0(x0, Pos(x1), Pos(x2), ty_Int)
new_primPlusNat0(Zero, Succ(x0))
new_primMinusNat0(Zero, Succ(x0))
new_span2Zs1([])
new_readInt0(x0, x1, x2, ty_Integer)
new_readInt0(x0, Neg(x1), Pos(x2), ty_Int)
new_readInt0(x0, Pos(x1), Neg(x2), ty_Int)
new_primMinusNat0(Succ(x0), Succ(x1))
new_pt(x0, ty_Int)
new_span2Zs05(x0, x1, Succ(x2), Succ(x3), x4)
new_pt(x0, ty_Integer)
new_primPlusNat0(Zero, Zero)
new_span2Zs09(x0, x1, Succ(x2), Zero)
new_primMulNat0(Zero, x0)
new_span2Zs07(x0, x1)
new_span2Zs05(x0, x1, Zero, Zero, x2)
new_span2Zs09(x0, x1, Succ(x2), Succ(x3))
new_primMulNat0(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr(yv59, yv60, yv61, Succ(yv620), Succ(yv630), ba) → new_foldr(yv59, yv60, yv61, yv620, yv630, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr0(yv28, yv29, yv30, Succ(yv310), Succ(yv320), yv33, ba) → new_foldr0(yv28, yv29, yv30, yv310, yv320, yv33, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: